package bcontractor.api;

/**
 * Interface that must be implemented by a reasoner
 * 
 * @author lundberg
 * 
 */
public interface SATReasoner<S extends Sentence<S>> {

    /**
     * Verifies if the given sentense set entails a given sentence.
     * 
     * @param sentences
     *            sentense set
     * @param sentence
     *            sentence
     * @return true if the sentence is entailed, false otherwise
     */
    boolean entails(SentenceSet<S> sentences, S sentence);

    /**
     * Verifies if the given sentence set is unsatisfiable.
     * 
     * @param sentences
     *            sentences
     * @return true if it is unsatisfiable, false otherwise
     */
    boolean isUnsatisfiable(SentenceSet<S> sentences);

    /**
     * Verifies if the given sentence set is satisfiable.
     * 
     * @param sentences
     *            sentences
     * @return true if it is satisfiable, false otherwise
     */
    boolean isSatisfiable(SentenceSet<S> sentences);
}